[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
apersistence_io
using ebm-vol-inv
,
address
,
nat-list-less
,
lp-array
procedures apersistence_io_commit# lp-array × address × nat × avolume : nat-set × address × nat × nat-list × lp-array × nat-set : error
nondeterministic;
apersistence_io_requires_commit# address × nat × nat-list × avolume × lp-array × nat-set : : bool nondeterministic;
apersistence_io_add_log_leb# nat × address × nat × avolume × lp-array × nat-set : nat-list : error nondeterministic;
apersistence_io_format# nat × nat × lp-array × address × nat : : address × nat × nat-list × avolume × lp-array × nat-set × error
nondeterministic;
apersistence_io_recover#
: address × nat × nat-set × nat-list × lp-array × address × nat × nat-list × lp-array × nat-set × avolume : error
nondeterministic;
apersistence_io_get_volume_size# address × nat × nat-list × avolume × lp-array × nat-set : : nat ;
apersistence_io_get_page_size# address × nat × nat-list × avolume × lp-array × nat-set : : nat ;
apersistence_io_get_leb_size# address × nat × nat-list × avolume × lp-array × nat-set : : nat ;
apersistence_io_write# nat × nat × nat × nat × buffer × address × nat × nat-list × lp-array × nat-set : avolume : error
nondeterministic;
apersistence_io_read# nat × nat × nat × nat × address × nat × nat-list × avolume × lp-array × nat-set : buffer : error
nondeterministic;
apersistence_io_remap# nat × address × nat × nat-list × lp-array × nat-set : avolume : error nondeterministic;
apersistence_io_unmap# nat × address × nat × nat-list × lp-array × nat-set : avolume nonfunctional ;
variables PVOL : avolume flexible;
BUF : buffer flexible;
BUF0 : buffer flexible;
N : nat flexible;
N0 : nat flexible;
N1 : nat flexible;
LNUM : nat flexible;
OFFSET : nat flexible;
ISBUF : bool flexible;
isbuf : bool;
ERR : error flexible;
ERR0 : error flexible;
VOLSIZE : nat flexible;
SIZE : nat flexible;
PROOTADR : address flexible;
PROOTADR0 : address flexible;
PMAXINO : nat flexible;
PMAXINO0 : nat flexible;
COMMIT? : bool flexible;
PLOG : nat-list flexible;
LOG : nat-list flexible;
plog : nat-list;
log : nat-list;
LPT : lp-array flexible;
PLPT : lp-array flexible;
ORPHANS : nat-set flexible;
PORPHANS : nat-set flexible;
state variables PROOTADR : address flexible;
PMAXINO : nat flexible;
PLOG : nat-list flexible;
PVOL : avolume flexible;
PLPT : lp-array flexible;
PORPHANS : nat-set flexible;
initialization procedure apersistence_io_format#
if ERR = ESUCCESS
sequential
invariants inv : ⊦ ebm-vol-inv(PVOL);
lpt-size : ⊦ # PLPT = # PVOL;
crash predicate PROOTADR = PROOTADR` ∧ PMAXINO = PMAXINO` ∧ PLOG = PLOG` ∧ PLPT = PLPT` ∧ PVOL` ⊆ PVOL ∧ PORPHANS = PORPHANS`
with crash-neutrality
recovery procedure apersistence_io_recover#
if ERR = ESUCCESS
declarations commit:
apersistence_io_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; ERR)
precondition # LPT = # PVOL;
postcondition true;
{if # LPT = # PVOL
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then {PROOTADR := PROOTADR0; PMAXINO := PMAXINO0; PLOG := []; PLPT := LPT; PORPHANS := ORPHANS}; ORPHANS := ?}
else abort
}
requires-commit:
apersistence_io_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?)
precondition true;
postcondition true;
{COMMIT? := ?
}
add-log-leb:
apersistence_io_add_log_leb#(LNUM, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; PLOG; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then PLOG := PLOG + LNUM}
}
format:
apersistence_io_format#(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; ; PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, ERR)
precondition # LPT = VOLSIZE ∧ SIZE = LEB_SIZE;
postcondition true;
{if # LPT = VOLSIZE ∧ SIZE = LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {PVOL := fill(mkavolume(VOLSIZE), unmapped); PROOTADR := PROOTADR0; PMAXINO := PMAXINO0; PLOG := []; PLPT := LPT;
PORPHANS := ∅}
else PVOL := ?, PROOTADR := ?, PMAXINO := ?, PLOG := ?, PLPT := ?, PORPHANS := ?}
else abort
}
recover:
apersistence_io_recover#(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, PVOL; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then PROOTADR0 := PROOTADR, PMAXINO0 := PMAXINO, LOG := PLOG, LPT := PLPT, ORPHANS := PORPHANS
else PVOL := ?, PROOTADR := ?, PMAXINO := ?, PLOG := ?, PLPT := ?, PROOTADR0 := ?, PMAXINO0 := ?, LOG := ?, LPT := ?, ORPHANS := ?,
PORPHANS := ?}
}
get-volume-size:
apersistence_io_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
precondition true;
postcondition true;
{N := # PVOL
}
get-page-size:
apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
precondition true;
postcondition true;
{N := EB_PAGE_SIZE
}
get-leb-size:
apersistence_io_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)
precondition true;
postcondition true;
{N := LEB_SIZE
}
write:
apersistence_io_write#(LNUM, OFFSET, N0, N, BUF, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR)
precondition LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ # PVOL[LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
;
postcondition true;
{if LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ # PVOL[LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE)
∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then if N ≠ 0 then PVOL[LNUM] := mapped(PVOL[LNUM].data + mkempbuf(OFFSET - # PVOL[LNUM].data) + subarray(BUF, N0, N))
else choose N1
with N1 < N ∧ is-aligned(N1, EB_PAGE_SIZE)
in if N1 ≠ 0 then PVOL[LNUM] := mapped(PVOL[LNUM].data + mkempbuf(OFFSET - # PVOL[LNUM].data) + subarray(BUF, N0, N1))
ifnone skip}
else abort
}
read:
apersistence_io_read#(LNUM, OFFSET, N0, N, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR)
precondition LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE;
postcondition true;
{if LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then BUF := copy(PVOL[LNUM].data + mkempbuf(LEB_SIZE - # PVOL[LNUM].data), OFFSET, BUF, N0, N)
else choose BUF0
with # BUF0 = # BUF ∧ range=(BUF, 0, BUF0, 0, N0) ∧ range=(BUF, N0 + N, BUF0, N0 + N, # BUF - N0 + N)
in BUF := BUF0}
else abort
}
remap:
apersistence_io_remap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR)
precondition LNUM < # PVOL;
postcondition true;
{if LNUM < # PVOL
then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PVOL[LNUM] := mapped(mkbuf(0)) else {skip or PVOL[LNUM] := unmapped}}
else abort
}
unmap:
apersistence_io_unmap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL)
precondition LNUM < # PVOL;
postcondition true;
{if LNUM < # PVOL then PVOL[LNUM] := unmapped else abort
}
end data asm specification